T:Type. AtomFree(Type;T)  (L:T List, a:Atom1. (x:T. (x  L) & x:T>>a)  L:T List>>a) 

latex

Definitions	x:A. B(x), P  Q, P  Q, x:A. B(x), P & Q, P  Q, t  T, Prop, if b t else f fi, true, false, T, True, P  Q, x. t(x), {T}, A & B, (x  l), , Unit, , AB, A, False, x(s),
Lemmas	l member wf, inheres wf, atom-free wf, inl-inherence, unit wf, lt int wf, length wf1, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le int wf, le wf, bnot wf, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, inherence-ap-elim, select wf, nat wf, inherence-trivial, exists functionality wrt iff, and functionality wrt iff, cons member